Theorem 3impia 1135

Description: Importation to triple conjunction. (Contributed by NM, 13-Jun-2006.) (Proof shortened by Wolf Lammen, 21-Jun-2022.)

Hypothesis

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

Assertion

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

Proof of Theorem 3impia

Step	Hyp	Ref	Expression
1		3impia.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
2	1	expimpd 459	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	3impib 1134	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:  mopick2  2665  ceqsalt  3487  3gencl  3497  vtoclgft  3519  rspc6v  3600  mob2  3676  moi  3679  reupick3  4278  disjne  4411  elpr2elpr  4829  disji2  5092  disji  5093  tz7.2  5641  sofld  6197  ordintdif  6440  funopg  6602  fvun1  7007  fvopab6  7059  fveqressseq  7111  fvcofneq  7125  fprg  7191  isores3  7374  ovmpt4g  7599  ovmpos  7600  ov2gf  7601  ofrval  7737  sorpssuni  7780  sorpssint  7781  poxp  8177  poseq  8212  suppss2  8255  frrlem12  8353  smoel  8406  smoord  8411  smogt  8413  oaass  8607  oewordi  8638  oeoalem  8643  oeoelem  8645  nnawordi  8668  nnaass  8669  naddssim  8733  qsel  8855  xpdom3  9132  onsdominel  9183  mapdom3  9206  sdomdomtrfi  9254  domsdomtrfi  9255  php  9260  onomeneq  9267  fisseneq  9292  fodomfir  9357  cantnflem1  9727  ttrclss  9758  cfslbn  10384  cfsmolem  10387  cfcoflem  10389  infpssrlem4  10423  fin23lem7  10433  fin23lem25  10441  isf34lem7  10496  hsmexlem2  10544  axcc3  10555  axdc4lem  10572  tskss  10882  gruss  10920  gruurn  10922  gruiun  10923  gruel  10927  gruen  10936  grudomon  10941  grothac  10954  axpre-sup  11293  axsup  11424  addn0nid  11775  letrp1  12201  p1le  12202  lemul1a  12211  infrelb  12342  nnadddir  12434  zextle  12812  zextlt  12813  btwnnz  12815  gtndiv  12816  uzind2  12832  fzind  12837  zsupss  13104  xrltne  13332  lemaxle  13365  qbtwnre  13369  qbtwnxr  13370  xlemul1a  13458  icogelb  13567  iccleub  13572  iccsplit  13656  uzsubsubfz  13720  elfz0fzfz0  13807  difelfznle  13816  fvffz0  13820  elfzo0le  13878  fzonmapblen  13883  fzofzim  13884  ceile  14029  modadd1  14088  muladdmodid  14093  modmul1  14107  modirr  14125  fsuppmapnn0fiub0  14176  expcl2lem  14256  expclzlem  14266  expnegz  14279  leexp2r  14357  bcval4  14492  bccmpl  14494  hashbnd  14521  hashunsnggt  14579  hashgt23el  14610  hashfundm  14628  elovmpowrd  14744  ccatval2  14764  ccatrcl1  14782  wrdl1s1  14804  ccat2s1fvw  14828  swrdsb0eq  14855  swrdccatin1  14916  pfxccatpfx2  14928  repswswrd  14977  cshwcsh2id  15021  sgn3da  15297  absexpz  15515  climbdd  15883  iseraltlem2  15894  binomfallfac  16251  dvdsle  16524  divalgb  16618  ndvdssub  16623  dvdsgcd  16761  dfgcd2  16763  rplpwr  16776  nn0rppwr  16779  nn0expgcd  16782  lcmgcdlem  16825  lcmfunsn  16863  coprmdvds1  16871  qredeq  16876  2mulprm  16912  prmdvdsexpr  16937  nnnn0modprm0  17028  prm23ge5  17037  pcexp  17081  difsqpwdvds  17109  prmpwdvds  17126  ramcl  17251  cshwshashlem3  17319  cshwrepswhash1  17324  elrestr  17649  mreintcl  17815  mremre  17824  mrieqv2d  17863  initoeu2lem1  18239  funcestrcsetclem9  18372  funcsetcestrclem9  18387  prstr  18523  drsdirfi  18529  latnlej  18680  latnlej2  18683  acsdrsel  18767  acsdrscl  18770  mrelatglb  18784  mrelatlub  18786  isnmgm  18870  grpasscan1  19262  grpinvnz  19270  mulgneg2  19368  gsmsymgrfix  19693  f1omvdco2  19713  symggen  19735  odcl2  19830  odhash3  19841  lsmss1  19930  lsmss2  19932  efgred  20013  efgcpbl  20021  ablfacrp  20333  ablfac1eu  20340  ablfaclem3  20354  omndadd  20393  ogrpaddlt  20403  dvdsrmul1  20650  dvdsunit  20660  irredmul  20710  c0snmgmhm  20743  lmodlema  21191  psgnodpmr  21951  phlssphl  22020  lindsss  22185  lindfmm  22188  ply1scln0  22665  dmatelnd  22866  mdetdiaglem  22968  mdet0  22976  mdetunilem7  22988  slesolinv  23053  cramerimplem3  23058  cpmatpmat  23083  m2cpminvid2lem  23127  chfacfscmul0  23231  chfacfpmmul0  23235  riinopn  23281  clsndisj  23448  cnpf2  23623  hausnei2  23726  cmpcov  23762  cmpfii  23782  unconn  23802  t1connperf  23809  nrmr0reg  24123  fbfinnfr  24215  filuni  24259  alexsubALT  24425  tmdgsum  24469  cuspcvg  24674  mopni  24866  isngp4  24986  metdsre  25228  iimulcl  25313  phtpc01  25372  clmmulg  25477  cfilucfil4  25697  bcthlem5  25704  bcth  25705  bcth3  25707  itg1le  26089  itg2le  26115  bddmulibl  26214  bddiblnc  26217  dvnres  26306  cpnord  26310  dvnfre  26327  deg1ge  26471  dgr1term  26634  aaliou3lem2  26727  sincosq1lem  26883  cxpge0  27068  cxpmul2  27074  logrec  27148  logbgcd1irr  27179  sqfpc  27521  bcmono  27661  gausslemma2dlem1a  27749  gausslemma2dlem2  27751  gausslemma2dlem4  27753  2lgsoddprmlem3  27798  pntrmax  27948  qabvexp  28010  ostth2lem2  28018  fltoprmlem2  28051  nosepon  28079  nolesgn2o  28085  nogesgn1o  28087  nosepnelem  28093  nosepne  28094  nosepdmlem  28097  nosepdm  28098  nodenselem8  28105  noresle  28111  noetasuplem4  28150  noetainflem4  28154  cutbdaylt  28241  eqcuts3  28247  addsuniflem  28444  sltmuls1  28590  precsexlem6  28655  precsexlem7  28656  precsexlem11  28660  ltonold  28704  onnolt  28709  n0fincut  28798  oldfib  28820  expadds  28878  ax5seglem4  29567  axeuclidlem  29597  uhgredgrnv  29765  usgredg4  29855  nbuhgr2vtx1edgblem  29989  vtxduhgr0e  30116  vtxduhgr0nedg  30130  rusgrpropnb  30221  uspgr2wlkeqi  30285  redwlklem  30307  lfgrwlkprop  30327  2pthnloop  30374  spthonepeq  30395  pthdlem2lem  30410  crctcshwlkn0lem3  30458  crctcshwlkn0lem5  30460  crctcshwlkn0lem7  30462  crctcshwlkn0  30467  wlkiswwlks1  30513  wlkiswwlks2  30521  wlkiswwlksupgr2  30523  wwlksnext  30539  wwlksnextproplem2  30556  wspthsnonn0vne  30563  2pthon3v  30589  rusgrnumwwlk  30624  erclwwlkeqlen  30667  erclwwlksym  30669  erclwwlktr  30670  erclwwlkneqlen  30716  erclwwlknsym  30718  erclwwlkntr  30719  uhgr3cyclex  30840  upgreupthseg  30867  eupth2lem3lem4  30889  eucrctshift  30901  4cycl2vnunb  30948  nvs  31322  nvtri  31329  nmlno0  31454  nmlnoubi  31455  ubth  31532  hlipgt0  31573  ocnel  31957  elspansn2  32226  elspansn3  32231  normcan  32235  pjoml2  32270  lecm  32276  osum  32304  nmbdfnlb  32709  leopmul  32793  hstpyth  32888  cvnbtwn  32945  ssmd1  32970  ssmd2  32971  ssdmd1  32972  ssdmd2  32973  cvmd  32995  cvdmd  32996  superpos  33013  disji2f  33269  disjif  33270  disjif2  33273  preiman0  33400  padct  33407  ffs2  33415  bcm1n  33483  s2f1  33606  archiabl  33858  slmdlema  33863  lbslsat  34359  eulerpartlemb  35111  nelscottrankgt  35874  acwer1prc  35893  onprcf1acwevdlem1  36086  fisshasheq  36101  cvmsdisj  36243  cvmlift2lem12  36287  satfrel  36340  satfrnmapom  36343  fmlasuc  36359  satffun  36382  satef  36389  sategoelfv  36393  elpssmo  36673  lineintmo  37137  nmuladdss  37177  nn0prpwlem  37325  nn0prpw  37326  neibastop2lem  37363  tr0elw  37487  lindsadd  38804  areacirc  38899  incsequz  38948  mettrifi  38957  ismtybnd  39007  heiborlem1  39011  rngoisocnv  39181  risci  39187  eqvrelqsel  39898  lfl1  40393  lkrlsp2  40426  omlfh3N  40582  cvrnbtwn  40594  cvrnbtwn2  40598  cvrnbtwn4  40602  cvlexch3  40655  cvlexch4N  40656  cvlatexchb1  40657  2llnne2N  40731  atcvrj0  40751  cvrat2  40752  ps-1  40800  3atlem5  40810  islln2a  40840  lplnriaN  40873  lplnribN  40874  llncvrlpln2  40880  lplncvrlvol2  40938  psubatN  41078  pmapglb2N  41094  pmapglb2xN  41095  2llnma1b  41109  paddasslem17  41159  pmod2iN  41172  pmodl42N  41174  hlmod1i  41179  atmod1i1  41180  atmod1i2  41182  llnmod1i2  41183  pclcmpatN  41224  osumcllem8N  41286  pexmidlem3N  41295  pl42lem4N  41305  4atexlem7  41398  ltrnnid  41459  cdlemc4  41517  cdleme32a  41764  cdlemeg46gfre  41855  cdlemf2  41885  cdlemg4c  41935  trlcoat  42046  tendovalco  42088  tendoeq2  42097  cdlemk36  42236  diael  42366  diatrl  42367  dicelval1stN  42511  dicelval2nd  42512  dihlspsnat  42656  dochkr1  42801  lcfrlem9  42873  mapdh8e  43107  hdmapval0  43156  hgmapval0  43215  dvdsexpnn0  43652  incssnn0  43988  pell14qrexpcl  44140  pell14qrgap  44148  congadd  44239  acongsym  44249  acongtr  44251  dvdsacongtr  44257  jm2.19lem3  44264  jm2.19lem4  44265  jm2.26lem3  44274  onexlimgt  44506  nadd2rabex  44649  ismnushort  45546  bi13impia  45732  3impcombi  46059  ioogtlb  46780  iocgtlb  46787  iocleub  46788  icoltub  46793  iooltub  46795  limclner  46934  limsupre3lem  47015  climuzlem  47026  fsupdm  48125  finfdm  48129  elfzelfzlble  48664  subsubelfzo0  48670  m1modnep2mod  48701  m1modmmod  48707  modlt0b  48712  mod2addne  48713  iccpartigtl  48778  sqrtpwpw2p  48896  fmtnoprmfac1lem  48922  fmtno4prmfac  48930  evenltle  49088  even3prm2  49090  wtgoldbnnsum4prm  49173  bgoldbnnsum3prm  49175  bgoldbtbndlem1  49176  bgoldbtbndlem3  49178  bgoldbtbndlem4  49179  bgoldbtbnd  49180  uhgrimisgrgriclem  49301  isubgr3stgrlem7  49343  clnbgr3stgrgrlic  49391  gpgedg2iv  49438  pgnbgreunbgrlem3  49489  pgnbgreunbgrlem6  49495  upgrwlkupwlk  49511  funcringcsetcALTV2lem9  49668  funcringcsetclem9ALTV  49691  lincscmcl  49875  lindslinindimp2lem4  49904  lincresunit2  49921  lincresunit3  49924  elfzolborelfzop1  49962  rege1logbzge0  50002  fllog2  50011  dignn0ldlem  50045  rrx2pnecoorneor  50159  rrx2plord2  50166  rrx2linest  50185  itscnhlinecirc02p  50228  ipolub  50433  ipoglb  50436