Theorem 3impib 1117

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

Syntax hints:   → wi 4   ∧ wa 397   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  3impia  1118  mob  3714  eqreu  3726  dedth3h  4589  prproe  4907  rbropap  5566  breldmg  5910  ssimaexg  6978  funopdmsn  7148  fpr3g  8270  wfr3g  8307  dfsmo2  8347  omwordri  8572  3ecoptocl  8803  ttrclselem2  9721  frr3g  9751  cfslb  10261  cofsmo  10264  cfsmolem  10265  coftr  10268  domtriomlem  10437  zorn2lem7  10497  ttukey2g  10511  gchi  10619  tskxpss  10767  tskord  10775  infm3  12173  uzind  12654  fzind  12660  fnn0ind  12661  xltnegi  13195  axdc4uz  13949  facwordi  14249  swrdnd2  14605  cshwidxmod  14753  relexpsucl  14978  relexpsucr  14979  relexprelg  14985  relexpaddnn  14998  caubnd  15305  mulgcd  16490  lcmfdvds  16579  lcmfdvdsb  16580  coprmdvds1  16589  pcfac  16832  ramz  16958  imasleval  17487  cictr  17752  initoeu2lem1  17964  drsdir  18255  psasym  18529  pstr  18530  tsrlin  18538  dirge  18556  mgmcl  18564  mhmlin  18679  mhmmulg  18995  issubg2  19021  nsgbi  19037  gsumcom2  19843  srgmulgass  20040  dvdsrtr  20182  issubrg2  20339  drnginvrcl  20379  drnginvrn0  20380  drnginvrl  20382  drnginvrr  20383  isdrngd  20390  isdrngdOLD  20392  abvmul  20437  abvtri  20438  lmhmlin  20646  domnmuln0  20914  ipcj  21187  cssincl  21241  obsip  21276  decpmatmulsumfsupp  22275  mp2pm2mplem4  22311  pm2mpghm  22318  pm2mpmhmlem1  22320  inopn  22401  basis1  22453  iscldtop  22599  2ndcdisj  22960  cnmpt2t  23177  cnmpt22  23178  cnmptcom  23182  fbasssin  23340  ptcmplem3  23558  xmeteq0  23844  prdsxmslem2  24038  nmvs  24193  nmolb  24234  volfiniun  25064  sincosq1sgn  26008  sincosq2sgn  26009  sincosq3sgn  26010  sincosq4sgn  26011  addsproplem2  27454  negsproplem2  27503  negsid  27515  mulsproplem9  27580  precsexlem10  27662  ewlkle  28862  wwlksnext  29147  umgr2adedgwlklem  29198  elwwlks2ons3im  29208  umgrwwlks2on  29211  conngrv2edg  29448  frgrwopregasn  29569  frgrwopregbsn  29570  frgrwopreglem5  29574  frgrwopreglem5ALT  29575  frgr2wwlkeu  29580  ablocom  29801  nmcvcn  29948  ipassi  30094  htth  30171  shaddcl  30470  shmulcl  30471  shsubcl  30473  chlimi  30487  pjspansn  30830  cnopc  31166  cnfnc  31183  adj1  31186  lnfnmul  31301  atord  31641  atcvat2  31642  cdj3i  31694  nexple  33007  signstfvc  33585  bnj910  33959  bnj1154  34010  umgr2cycllem  34131  pconncn  34215  mrsubccat  34509  shftvalg  34701  linethru  35125  sin2h  36478  cos2h  36479  tan2h  36480  dvasin  36572  areacirclem1  36576  riotasv  37829  lsmsatcv  37880  omllaw  38113  2llnjN  38438  dalawlem10  38751  dalawlem13  38754  dalawlem14  38755  pclfinclN  38821  ismrc  41439  fzsplit1nn0  41492  pell1234qrmulcl  41593  pell14qrmulcl  41601  onsucf1olem  42020  iunrelexp0  42453  bi23impib  43246  bi13impib  43247  trelded  43326  suctrALT  43587  suctrALTcf  43683  suctrALTcfVD  43684  stoweidlem17  44733  zm1nn  46010  bgoldbtbndlem4  46476  bgoldbtbnd  46477  tgblthelfgott  46483  mgmhmlin  46556  issubmgm2  46560  clcllaw  46601  rnghmmul  46698  issubrng2  46737  ztprmneprm  47023  lcoel0  47109  linindslinci  47129  fv2arycl  47334