Theorem 3impib 1112

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 418	. 2 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))
3	2	3imp 1107	1 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 398   ∧ w3a 1083

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 209  df-an 399  df-3an 1085

This theorem is referenced by:  3impia  1113  mob  3708  eqreu  3720  dedth3h  4525  prproe  4830  rbropap  5443  breldmg  5773  ssimaexg  6744  funopdmsn  6907  wfr3g  7947  dfsmo2  7978  omwordri  8192  3ecoptocl  8383  cfslb  9682  cofsmo  9685  cfsmolem  9686  coftr  9689  domtriomlem  9858  zorn2lem7  9918  ttukey2g  9932  gchi  10040  tskxpss  10188  tskord  10196  infm3  11594  uzind  12068  fzind  12074  fnn0ind  12075  xltnegi  12603  axdc4uz  13346  facwordi  13643  swrdnd2  14011  cshwidxmod  14159  relexpsucr  14382  relexpsucl  14386  relexprelg  14391  relexpaddnn  14404  caubnd  14712  mulgcd  15890  lcmfdvds  15980  lcmfdvdsb  15981  coprmdvds1  15990  pcfac  16229  ramz  16355  imasleval  16808  cictr  17069  initoeu2lem1  17268  drsdir  17539  psasym  17814  pstr  17815  tsrlin  17823  dirge  17841  mgmcl  17849  mhmlin  17957  mhmmulg  18262  issubg2  18288  nsgbi  18303  cygablOLD  19005  gsumcom2  19089  srgmulgass  19275  dvdsrtr  19396  drnginvrcl  19513  drnginvrn0  19514  drnginvrl  19515  drnginvrr  19516  isdrngd  19521  issubrg2  19549  abvmul  19594  abvtri  19595  lmhmlin  19801  domnmuln0  20065  ipcj  20772  cssincl  20826  obsip  20859  decpmatmulsumfsupp  21375  mp2pm2mplem4  21411  pm2mpghm  21418  pm2mpmhmlem1  21420  inopn  21501  basis1  21552  iscldtop  21697  2ndcdisj  22058  cnmpt2t  22275  cnmpt22  22276  cnmptcom  22280  fbasssin  22438  ptcmplem3  22656  xmeteq0  22942  prdsxmslem2  23133  nmvs  23279  nmolb  23320  volfiniun  24142  sincosq1sgn  25078  sincosq2sgn  25079  sincosq3sgn  25080  sincosq4sgn  25081  ewlkle  27381  wwlksnext  27665  umgr2adedgwlklem  27717  elwwlks2ons3im  27727  umgrwwlks2on  27730  conngrv2edg  27968  frgrwopregasn  28089  frgrwopregbsn  28090  frgrwopreglem5  28094  frgrwopreglem5ALT  28095  frgr2wwlkeu  28100  ablocom  28319  nmcvcn  28466  ipassi  28612  htth  28689  shaddcl  28988  shmulcl  28989  shsubcl  28991  chlimi  29005  pjspansn  29348  cnopc  29684  cnfnc  29701  adj1  29704  lnfnmul  29819  atord  30159  atcvat2  30160  cdj3i  30212  nexple  31263  signstfvc  31839  bnj910  32215  bnj1154  32266  umgr2cycllem  32382  pconncn  32466  mrsubccat  32760  shftvalg  32958  frr3g  33116  fpr3g  33117  linethru  33609  sin2h  34876  cos2h  34877  tan2h  34878  dvasin  34972  areacirclem1  34976  riotasv  36089  lsmsatcv  36140  omllaw  36373  2llnjN  36697  dalawlem10  37010  dalawlem13  37013  dalawlem14  37014  pclfinclN  37080  ismrc  39291  fzsplit1nn0  39344  pell1234qrmulcl  39445  pell14qrmulcl  39453  iunrelexp0  40040  bi23impib  40812  bi13impib  40813  trelded  40892  suctrALT  41153  suctrALTcf  41249  suctrALTcfVD  41250  stoweidlem17  42295  zm1nn  43495  bgoldbtbndlem4  43966  bgoldbtbnd  43967  tgblthelfgott  43973  mgmhmlin  44046  issubmgm2  44050  clcllaw  44091  rnghmmul  44164  ztprmneprm  44388  lcoel0  44476  linindslinci  44496