Theorem 3impib 1134

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.)

Hypothesis

Ref	Expression
3impib.1	⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))

Assertion

Ref	Expression
3impib	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Proof of Theorem 3impib

Step	Hyp	Ref	Expression
1		3impib.1	. . 3 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
2	1	expd 421	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1128	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  3impia  1135  mob  3678  eqreu  3690  dedth3h  4546  prproe  4868  rbropap  5546  breldmg  5897  ssimaexg  6968  funopdmsn  7151  fpr3g  8288  wfr3g  8322  dfsmo2  8340  omwordri  8563  3ecoptocl  8813  ttrclselem2  9709  frr3g  9742  cfslb  10272  cofsmo  10275  cfsmolem  10276  coftr  10279  domtriomlem  10448  zorn2lem7  10508  ttukey2g  10522  gchi  10637  tskxpss  10785  tskord  10793  infm3  12202  uzind  12717  fzind  12723  fnn0ind  12724  xltnegi  13272  axdc4uz  14052  facwordi  14357  swrdnd2  14729  cshwidxmod  14878  relexpsucl  15108  relexpsucr  15109  relexprelg  15115  relexpaddnn  15128  caubnd  15450  mulgcd  16644  lcmfdvds  16738  lcmfdvdsb  16739  coprmdvds1  16748  pcfac  16997  ramz  17123  imasleval  17633  cictr  17900  initoeu2lem1  18109  drsdir  18396  psasym  18670  pstr  18671  tsrlin  18679  dirge  18697  mgmcl  18739  mgmhmlin  18807  issubmgm2  18811  mhmlin  18907  mhmmulg  19244  issubg2  19271  nsgbi  19286  gsumcom2  20108  srgmulgass  20362  dvdsrtr  20515  rnghmmul  20596  issubrng2  20726  issubrg2  20760  domnmuln0  20877  drnginvrcl  20926  drnginvrn0  20927  drnginvrl  20929  drnginvrr  20930  isdrngd  20937  isdrngdOLD  20939  abvmul  20993  abvtri  20994  lmhmlin  21225  ipcj  21853  cssincl  21907  obsip  21940  decpmatmulsumfsupp  23004  mp2pm2mplem4  23040  pm2mpghm  23047  pm2mpmhmlem1  23049  inopn  23130  basis1  23181  iscldtop  23326  2ndcdisj  23688  cnmpt2t  23905  cnmpt22  23906  cnmptcom  23910  fbasssin  24068  ptcmplem3  24286  xmeteq0  24570  prdsxmslem2  24761  nmvs  24908  nmolb  24949  volfiniun  25781  sincosq1sgn  26743  sincosq2sgn  26744  sincosq3sgn  26745  sincosq4sgn  26746  addsproplem2  28243  negsproplem2  28302  negsid  28314  mulsproplem9  28397  precsexlem10  28489  uzsind  28678  recut  28767  ewlkle  30073  wwlksnext  30369  umgr2adedgwlklem  30420  elwwlks2ons3im  30430  usgrwwlks2on  30434  umgrwwlks2on  30435  conngrv2edg  30683  frgrwopregasn  30804  frgrwopregbsn  30805  frgrwopreglem5  30809  frgrwopreglem5ALT  30810  frgr2wwlkeu  30815  ablocom  31037  nmcvcn  31184  ipassi  31330  htth  31407  shaddcl  31706  shmulcl  31707  shsubcl  31709  chlimi  31723  pjspansn  32066  cnopc  32402  cnfnc  32419  adj1  32422  lnfnmul  32537  atord  32877  atcvat2  32878  cdj3i  32930  nexple  33311  signstfvc  35090  bnj910  35465  bnj1154  35516  r1filimi  35619  pconncn  35811  mrsubccat  36105  shftvalg  36319  linethru  36741  sin2h  38372  cos2h  38373  tan2h  38374  dvasin  38461  areacirclem1  38465  riotasv  39840  lsmsatcv  39891  omllaw  40124  2llnjN  40448  dalawlem10  40761  dalawlem13  40764  dalawlem14  40765  pclfinclN  40831  ismrc  43554  fzsplit1nn0  43607  pell1234qrmulcl  43704  pell14qrmulcl  43712  onsucf1olem  44119  iunrelexp0  44550  bi23impib  45317  bi13impib  45318  trelded  45396  suctrALT  45656  suctrALTcf  45752  suctrALTcfVD  45753  stoweidlem17  46853  zm1nn  48198  bgoldbtbndlem4  48732  bgoldbtbnd  48733  tgblthelfgott  48739  vopnbgrelself  48779  clnbgr3stgrgrlic  48944  clcllaw  49114  ztprmneprm  49285  lcoel0  49366  linindslinci  49386  fv2arycl  49586