Theorem hban 704

Description: If x is not free in φ and ψ, it is not free in (φ ∧ ψ).

Hypotheses

Ref	Expression
hb.1	⊢ (φ → ∀xφ)
hb.2	⊢ (ψ → ∀xψ)

Assertion

Ref	Expression
hban	⊢ ((φ ∧ ψ) → ∀x(φ ∧ ψ))

Proof of Theorem hban

Step	Hyp	Ref	Expression
1		hb.1	. . . 4 ⊢ (φ → ∀xφ)
2		hb.2	. . . . 5 ⊢ (ψ → ∀xψ)
3	2	hbne 699	. . . 4 ⊢ (¬ ψ → ∀x ¬ ψ)
4	1, 3	hbim 702	. . 3 ⊢ ((φ → ¬ ψ) → ∀x(φ → ¬ ψ))
5	4	hbne 699	. 2 ⊢ (¬ (φ → ¬ ψ) → ∀x ¬ (φ → ¬ ψ))
6		df-an 198	. 2 ⊢ ((φ ∧ ψ) ↔ ¬ (φ → ¬ ψ))
7	6	bial 695	. 2 ⊢ (∀x(φ ∧ ψ) ↔ ∀x ¬ (φ → ¬ ψ))
8	5, 6, 7	3imtr4 192	1 ⊢ ((φ ∧ ψ) → ∀x(φ ∧ ψ))

Syntax hints:  ¬ wn 1   → wi 2   ∧ wa 196  ∀wal 672

This theorem is referenced by:  hbbi 705  hb3an 707  19.21ad 741  eqvin.l1 851  hbsb4 905  ddelimf2 907  sbcom 916  cbval2 974  cbvex2 975  mopick 1054  hbel 1172  clelab 1187  bi2ralda 1232  hbrex 1238  hbrab 1311  cbvrex 1332  reu2 1338  eqvincf 1408  elrabf 1421  cbvrab 1425  axrep 1473  axrep2 1474  zfrep2 1475  zfrep3 1476  hbdif 1590  hbin 1647  hbuni 1925  eluniab 1926  reuuni2 1956  opabid 2099  cbvopab 2104  cbvopab1 2106  cbvopab1s 2107  hbopab 2111  onminex 2275  peano5 2394  hbxp 2444  hbco 2508  hbcnv 2516  hbima 2609  hbfun 2684  imadif 2714  hbfn 2720  hbf 2751  hbf1 2779  hbfo 2787  hbf1o 2798  fv3 2839  hbiso 2930  isotrALT 2936  tfr3 2964  hbrdg 2974  tz7.49 2997  cbvoprab12 3028  oprabval4g 3053  mapxpen 3390  xpmapenlem3 3393  xpmapenlem5 3395  nneneq 3408  ac6lem 3575  zornlem4 3606  zornlem5 3607  hta 3619  axextnd 3737  axrepndlem2 3739  axrepnd 3740  axunnd 3742  axpowndlem2 3744  axpowndlem4 3746  axpownd 3747  axregndlem2 3749  axregnd 3750  axinfndlem1 3751  axinfnd 3752  axacndlem4 3756  axacndlem5 3757  axacnd 3758  zfcndrep 3760  zfcndinf 3764  suppsr2 4017  suppsr3 4018  nnwof 4609

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6  ax-4 673  ax-5 674  ax-6 675  ax-gen 677

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org