Theorem 3impib 1115

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 207  df-an 396  df-3an 1088

This theorem is referenced by:  3impia  1116  mob  3725  eqreu  3737  dedth3h  4590  prproe  4909  rbropap  5574  breldmg  5922  ssimaexg  6994  funopdmsn  7169  fpr3g  8308  wfr3g  8345  dfsmo2  8385  omwordri  8608  3ecoptocl  8847  ttrclselem2  9763  frr3g  9793  cfslb  10303  cofsmo  10306  cfsmolem  10307  coftr  10310  domtriomlem  10479  zorn2lem7  10539  ttukey2g  10553  gchi  10661  tskxpss  10809  tskord  10817  infm3  12224  uzind  12707  fzind  12713  fnn0ind  12714  xltnegi  13254  axdc4uz  14021  facwordi  14324  swrdnd2  14689  cshwidxmod  14837  relexpsucl  15066  relexpsucr  15067  relexprelg  15073  relexpaddnn  15086  caubnd  15393  mulgcd  16581  lcmfdvds  16675  lcmfdvdsb  16676  coprmdvds1  16685  pcfac  16932  ramz  17058  imasleval  17587  cictr  17852  initoeu2lem1  18067  drsdir  18359  psasym  18633  pstr  18634  tsrlin  18642  dirge  18660  mgmcl  18668  mgmhmlin  18724  issubmgm2  18728  mhmlin  18818  mhmmulg  19145  issubg2  19171  nsgbi  19187  gsumcom2  20007  srgmulgass  20234  dvdsrtr  20384  rnghmmul  20465  issubrng2  20574  issubrg2  20608  domnmuln0  20725  drnginvrcl  20769  drnginvrn0  20770  drnginvrl  20772  drnginvrr  20773  isdrngd  20781  isdrngdOLD  20783  abvmul  20838  abvtri  20839  lmhmlin  21051  ipcj  21669  cssincl  21723  obsip  21758  decpmatmulsumfsupp  22794  mp2pm2mplem4  22830  pm2mpghm  22837  pm2mpmhmlem1  22839  inopn  22920  basis1  22972  iscldtop  23118  2ndcdisj  23479  cnmpt2t  23696  cnmpt22  23697  cnmptcom  23701  fbasssin  23859  ptcmplem3  24077  xmeteq0  24363  prdsxmslem2  24557  nmvs  24712  nmolb  24753  volfiniun  25595  sincosq1sgn  26554  sincosq2sgn  26555  sincosq3sgn  26556  sincosq4sgn  26557  ssltsn  27851  addsproplem2  28017  negsproplem2  28075  negsid  28087  mulsproplem9  28164  precsexlem10  28254  uzsind  28405  recut  28442  0reno  28443  ewlkle  29637  wwlksnext  29922  umgr2adedgwlklem  29973  elwwlks2ons3im  29983  umgrwwlks2on  29986  conngrv2edg  30223  frgrwopregasn  30344  frgrwopregbsn  30345  frgrwopreglem5  30349  frgrwopreglem5ALT  30350  frgr2wwlkeu  30355  ablocom  30576  nmcvcn  30723  ipassi  30869  htth  30946  shaddcl  31245  shmulcl  31246  shsubcl  31248  chlimi  31262  pjspansn  31605  cnopc  31941  cnfnc  31958  adj1  31961  lnfnmul  32076  atord  32416  atcvat2  32417  cdj3i  32469  nexple  33989  signstfvc  34567  bnj910  34940  bnj1154  34991  umgr2cycllem  35124  pconncn  35208  mrsubccat  35502  shftvalg  35711  linethru  36134  sin2h  37596  cos2h  37597  tan2h  37598  dvasin  37690  areacirclem1  37694  riotasv  38940  lsmsatcv  38991  omllaw  39224  2llnjN  39549  dalawlem10  39862  dalawlem13  39865  dalawlem14  39866  pclfinclN  39932  ismrc  42688  fzsplit1nn0  42741  pell1234qrmulcl  42842  pell14qrmulcl  42850  onsucf1olem  43259  iunrelexp0  43691  bi23impib  44482  bi13impib  44483  trelded  44562  suctrALT  44823  suctrALTcf  44919  suctrALTcfVD  44920  stoweidlem17  45972  zm1nn  47251  bgoldbtbndlem4  47732  bgoldbtbnd  47733  tgblthelfgott  47739  vopnbgrelself  47778  clnbgr3stgrgrlic  47914  clcllaw  48034  ztprmneprm  48191  lcoel0  48273  linindslinci  48293  fv2arycl  48497